a:, n:. (|a| < |n|)  ((a rem n) = a) 

latex

Up	int 2, int 2
Definitions	, t  T, P  Q, x:A. B(x), P & Q, P  Q, P  Q, , False, a  b  T , A, , P  Q, Dec(P), A  B, , S  T
Lemmas	nat plus wf, nat wf, absval wf, rem base case, nat plus inc, absval pos, decidable le, le wf, nat plus inc int nzero, rem sym 1a, minus minus cancel, absval sym, int nzero wf, rem sym 2